| Definitions | A & B, P & Q, Void, t  T,  x:A. B(x), Top,  x:A. B(x), P   Q, False,  b, x:A B(x), x:A  B(x),  A, True, {T}, SQType(T), Id, s = t, Prop, s ~ t, Atom$n,  , a = b, Type,  b, P  Q, Unit, left+right, es realizer ind Rpre compseq tag def, es realizer ind Rplus compseq tag def, R-has-loc(R;i), ecl-machine2(i;ds;da;x;T;ks;a;upd), ecl-machine3(ds;da;x;T;ks;a;snd), left  right, @loc precondition for a(v:T):P State(ds) v, let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), ecl-trans-tuple{i:l}(ds;da), ecl-trans(x), es realizer ind Rframe compseq tag def, es realizer ind Rinit compseq tag def, Knd, "$x", x : v, IdDeq, f g, Valtype(da;k), DeclaredType(ds;x), f(a), @loc effect knd(v:T) x := f State(ds) v , xL.R(x), @loc only events in L change x:T, @loc x initially v:T, R-state-var(i;ds;da;x;T;ks;tr), R-state-var-init(i;ds;da;x;T;v;ks;tr), ecl-machine1{$ecl:ut2}(i; ds; da; A), ecl-machine at i with state $eclAstate variables dsactions dasends sndupdates upd, f || g, if b t else f fi,  x. t(x), a:A fp B(a), ecl(ds;da), msg-spec(ds;da), update-spec(ds;da), update-spec-decl(upd;ds), msg-spec-loc-decl(snd;i;da), x.A(x), x dom(f), R-Feasible(R), State(ds), locl(a), KindDeq, f(x), A || B, f(x)?z, <a,b>, EqDecider(T), rec(x.A(x)), es realizer ind, type List,  x:A. B(x), (x l), Case b of inl(x) s(x) ; inr(y) t(y), i=j, Rsends-T(x1), Rsends-dt(x1), Rsends-l(x1), Rsends-knd(x1), Rsends?(x1), Reffect-T(x1), Reffect-knd(x1), Reffect?(x1), Rrframe-L(x1), Rpre-a(x1), Rpre-ds(x1), Rrframe-x(x1), Rrframe?(x1), Rpre?(x1), Rsends-ds(x1), Rbframe-L(x1), Rbframe-k(x1), Rbframe?(x1), Rsframe-L(x1), Rsends-g(x1), Rsframe-tag(x1), Rsframe-lnk(x1), Rsframe?(x1), Reffect-ds(x1), Raframe-L(x1), Reffect-x(x1), Raframe-k(x1), Raframe?(x1), Rframe-L(x1), Rframe-x(x1), Rframe?(x1), Rnone?(x1), Rplus-right(x1), Rplus-left(x1), Rplus?(x1), R-interface-compat(A;B), R-frame-compat(A;B), p = q, R-base-domain(R), Rda(R), Rds(R), R-loc(R), inr(x), IdLnk,  T, P Q, x(s), es realizer ind Reffect compseq tag def, {x:A| B(x) }, update-spec-vars(upd), nil, A/x,y. B(x;y), list_accum(x,a.f(x;a);y;l), Normal(T), xdom(f). v=f(x) P(x;v), Normal(ds), Dec(P), AtomFree(T;x), #$n, ||as||, a<b, A B,  ,  , l[i], 2of(t), 1of(t), product-deq(A;B;a;b), x,y. t(x;y), P  Q, msg-spec-links(snd), IdLnkDeq, remove-repeats(eq;L), ecl-tags(l;snd), source(l), es realizer ind Rsframe compseq tag def, only events in L send on lnk with tag, dt(l;da), isrcv_locl{isrcv_locl_compseq_tag_def:ObjectId}(a), lnk-decl(l;dt), es realizer ind Rsends compseq tag def, sends knd(v:T) on l:tagged(g,State(ds),v):dt, ecl-m3(a;snd;x;l), rcv(l,tg), S  T, S  T, R-lnk-tags(ds;da;l;tgs;ks;g) |
| Lemmas | R-lnk-tags wf, Rsends wf, ecl-m3 wf, fpf-cap-void-subtype, es-dt-cap, decl-type wf, rcv wf, lnk-decl wf, lnk-decl-compatible-single, es-dt wf, false wf, Rsframe wf, lsrc wf, ecl-tags wf, remove-repeats wf, idlnk-deq wf, msg-spec-links wf, fpf-join-dom2, or functionality wrt iff, fpf-single-dom, list accum wf, product-deq wf, pi1 wf, pi2 wf, subtype rel dep function, fpf-cap-join-subtype, R-state-var wf, nat wf, length wf1, select wf, fpf-compatible-single, R-state-var-compat-unequal-loc, l member subtype, fpf-compatible-single-iff, update-spec-vars wf, R-compat-Rall2, Reffect wf, Rpre wf, fpf-compatible-join2, fpf-compatible-singles, ma-valtype wf, assert-eq-knd, squash wf, true wf, IdLnk wf, fpf-compatible-symmetry, fpf-compatible-single2, fpf-empty-compatible-left, l member wf, fpf-join-cap-sq, top wf, fpf-cap-single, eqof eq btrue, ifthenelse wf, fpf-cap wf, decl-state-subtype, fpf-join wf, fpf-sub-join-left2, fpf-sub weakening, fpf-single wf, subtype rel self, deq wf, Knd sq, fpf-ap wf, Kind-deq wf, locl wf, fpf-compatible wf, decl-state wf, R-Feasible wf, ecl-machine wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, msg-spec-loc-decl wf, update-spec-decl wf, update-spec wf, msg-spec wf, ecl wf, Knd wf, fpf wf, ecl-disjoint-compatible, ecl-machine-loc, ecl-trans wf, ecl-trans-tuple wf, R-compat-disjoint, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, bnot wf, not wf, assert wf, eq id wf, bool wf, Id wf, Id sq, R-compat-symmetry, R-compat-Rplus-sq |
upd:update-spec(ds;da).